% EPC flow charts
% Author: Fabian Schuh
\documentclass{minimal}

\usepackage[utf8]{inputenc}
\usepackage[english, russian]{babel}


\usepackage{pgf}
\usepackage{tikz}
%%%<
\usepackage{verbatim}
\usepackage[active,tightpage]{preview}
\PreviewEnvironment{tikzpicture}
\setlength\PreviewBorder{5pt}%
%%%>

\usepackage[utf8]{inputenc}
\usetikzlibrary{arrows,automata}
\usetikzlibrary{positioning}


\tikzset{
    state/.style={
           rectangle,
           fill=blue!10,
           rounded corners,
           draw=black, very thick,
           minimum height=2em,
           inner sep=4pt,
           text centered,
           font=\fontsize{12}{14}\selectfont
           },	
     pil/.style={
           very thick,
           shorten <=1pt,
           shorten >=1pt}
}

\begin{document}

\begin{tikzpicture}[->,>=stealth']

 \node[state] (SAT) 
 {\begin{tabular}{l}
  \textbf{SAT}\\   
 \end{tabular}};


 \node[state, 
 right of=SAT, node distance=7.5cm
 ] (UP) 
 {\begin{tabular}{l}
  \textbf{Анализ формулы}
 \end{tabular}};

 \node[state, 
 right of=UP, node distance=4.5cm
 ] (ROLLBACK) 
 {\begin{tabular}{l}
  \textbf{Откат}   
 \end{tabular}};
 
  \node[state, 
 above of=ROLLBACK, node distance=3.5cm
 ] (UNSAT) 
 {\begin{tabular}{l}
  \textbf{UNSAT}   
 \end{tabular}};
 
  \node[state, 
 above of=UP, node distance=3.5cm
 ] (GUEES) 
 {\begin{tabular}{l}
  \textbf{Приcвоение переменной}\\
    \textbf{значения}
 \end{tabular}};
 
  \path (UP) edge[pil] node[anchor=south,text width=4cm]
                   {
                     нет конфликтов и
                     нет свободных переменных 
                   } (SAT)
   (UP) edge[pil, bend left] node[anchor=south]
                   {
                     конфликт                     
                   } (ROLLBACK)
   (ROLLBACK) edge[pil, bend left] (UP)
   (ROLLBACK) edge[pil] node[anchor=west, text width=4cm]
                   {
                     стек пуст
                   } (UNSAT)
   (UP) edge[pil, bend left] node[anchor=east, text width=2.5cm]
                   {
                     нет единичных дизъюнктов                     
                   } (GUEES)
                   
    (GUEES) edge[pil,bend left] (UP)
 ;
\end{tikzpicture}

\end{document}
